Nuprl Lemma : es-p-equiv_weakening
11,40
postcript
pdf
es
,
es'
:ES,
P
:(
es
:ES
E
). (
es
=
es'
)
es
es'
mod
es
,
e
.
P
(
es
,
e
)
latex
Definitions
x
:
A
.
B
(
x
)
,
E
,
t
T
,
f
(
a
)
,
x
(
s1
,
s2
)
,
ES
,
x
,
y
.
t
(
x
;
y
)
,
es
es'
mod
es
,
e
.
P
(
es
;
e
)
,
s
=
t
,
,
s
~
t
,
{
T
}
,
P
Q
,
SQType(
T
)
,
x
:
A
B
(
x
)
,
Type
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
P
&
Q
,
A
B
,
val(
e
)
val(
e'
)
,
(
e
<
e'
)
,
loc(
e
)
,
kind(
e
)
,
P
Q
,
P
Q
,
Knd
,
Id
Lemmas
es-kind
wf
,
es-loc
wf
,
es-causl
wf
,
es-same-val
wf
,
subtype
rel
self
,
event
system
wf
,
es-p-equiv
wf
,
es-E
wf
origin
es, es':ES, P:(es:ES
E
). (es = es') 
es 
es' mod es,e.P(es,e) es, es':ES, P:(es:ESE). (es = es') es es' mod es,e.P(es,e) x:A. B(x)
T
x,y. t(x;y) es' mod es,e.P(es;e) Q
B(x)B(x) B val(e')
Q Q